def val_is_var(val):
    return type(val) is str and (val[0].isupper() or val[0] == '_')

def val_is_const(val):
    return type(val) is str and val[0].islower()

fake_var_cnt = 0
def fake_var():
    global fake_var_cnt
    var = '_' + str(fake_var_cnt)
    fake_var_cnt += 1
    return var                

def unify_not_var(left, right, lbinds, rbinds):
    if type(left) is not type(right):
        return False   
    # constants
    if val_is_const(left):
        return left == right
    # lists
    if type(left) is not list:
        return False
    if len(left) != len(right):
        return False
    for new_left, new_right in zip(left, right):
        if not unify(new_left, new_right, lbinds, rbinds):
            return False
    return True

def propgate(var, val, lbinds, rbinds):
    if var in lbinds:
        propgate(lbinds[var], val, lbinds, rbinds)
        del lbinds[var]
    if var in rbinds:
        propgate(rbinds[var], val, lbinds, rbinds)
        del rbinds[var]
    for key, value in lbinds.items():
        if value == var:
            lbinds[key] = val
    for key, value in rbinds.items():
        if value == var:
            rbinds[key] = val
    
    

def unify(left, right, lbinds, rbinds):
    if not val_is_var(left):
        if not val_is_var(right):
            return unify_not_var(left, right, lbinds, rbinds)
        if not right in rbinds:
            rbinds[right] = left
            return True
        if not val_is_var(rbinds[right]):
            return unify_not_var(left, rbinds[right], lbinds, rbinds)
        propgate(rbinds[right], left, lbinds, rbinds)
        return True
    if not left in lbinds:
        if not val_is_var(right):
            lbinds[left] = right
            return True
        if not right in rbinds:
            lbinds[left] = rbinds[right] = fake_var()
            return True
        lbinds[left] = rbinds[right]
        return True
    if not val_is_var(lbinds[left]):
        if not val_is_var(right):
            return unify_not_var(lbinds[left], right, lbinds, rbinds)
        if not right in rbinds:
            rbinds[right] = lbinds[left]
            return True
        if not val_is_var(rbinds[right]):
            return unify_not_var(lbinds[left], rbinds[right], lbinds, rbinds)
        propgate(rbinds[right], lbinds[left], lbinds, rbinds)
        return True
    if not val_is_var(right):
        propgate(lbinds[left], right, lbinds, rbinds)
        return True
    if not right in rbinds:
        rbinds[right] = lbinds[left]
        return True
    # if not val_is_var(rbinds[right]):
    #     return propagate(lbinds[left], rbinds[right], lbinds, rbinds)

    propagate(lbinds[left], rbinds[right], lbinds, rbinds)
    return True

def options(binds):
    for val in binds.values():
        if not val_is_var(val):
            return True
    return False

def not1(val):
    if val is True:
        return False
    if val is False:
        return True
    # if val == 'either':
    #     return 'either'
    # if val == 'neither':
    #     return 'neither'
    # if val == 'unknown':
    #     return 'unknown'
    return val

def not2(val):
    if val is True:
        return 'fneither'
    if val is False:
        return 'tneither'
    if val is 'either':
        return 'neither'
    if val is 'neither':
        return 'either'
    if val is 'tneither':
        return False
    if val is 'fneither':
        return True
    # if val == 'unknown':
    # return 'unknown'
    return 'unknown'

def and1(val1, val2):
    if val1 == 'neither' or val2 == 'neither':
        return 'neither'
    if val1 == 'fneither' or val2 == 'fneither':
        return 'fneither'
    if val1 == 'unknown':
        if val2 is False:
            return 'fneither'
        return 'unknown'
    if val2 == 'unknown':
        if val1 is False:
            return 'fneither'
        return 'unknown'
    if val1 is False:
        if val2 == 'tneither':
            return 'fneither'
        return False
    if val2 is False:
        if val1 == 'tneither':
            return 'fneither'
        return False
    if val1 == 'tneither':
        if val2 == 'either':
            return 'unknown'
        return 'tneither'
    if val2 == 'tneither':
        if val1 == 'either':
            return 'unknown'
        return 'tneither'
    if val1 == 'either' or val2 == 'either':
        return 'either'
    return True

class Search:
    def __init__(self, base, query):
        self.query = query
        self.place = iter(base)
        self.up_binds = None
        self.scope = None
        self.op = None
        self.fate = False

    def scope_bind(self):
        new_binds = {}
        for key, value in self.up_binds.items():
            new_binds[key] = self.scope.bind(value)
        return new_binds

    def eval(self, expr, base, rbinds):
        if type(expr) is not list:
            return expr
        scope = Scope(base, expr, rbinds)
        return [scope.run(base), scope]
            
    def get(self, base):
        if self.op is not None:
            result = self.scope.run(base)
            if result is True:
                return self.scope_bind()
            if self.op == '=':
                if self.fate:
                    return result
            self.op = None
            self.up_binds = None
            self.scope = None
            
        for fact in self.place:
            lbinds = {}
            rbinds = {}
            if unify(self.query, fact[0], lbinds, rbinds):

                # The fate of this path is sealed
                if fact[1] != '<-' and not options(lbinds):
                    self.fate = True

                result = self.eval(fact[2], base, rbinds)

                if fact[1] == '=':
                    if type(result) is not list:
                        if result is True:
                            return lbinds
                        if not self.fate:
                            continue
                        return result
                    if result[0] is True:
                        self.op = '='
                        self.up_binds = lbinds
                        self.scope = result[1]
                        return self.scope_bind()
                    if not self.fate:
                        continue
                    return result[0]

                if fact[1] == '=!':
                    logic_val = None
                    if type(result) is not list:
                        logic_val = not1(result)
                    else:
                        logic_val = not1(result[0])
                    if logic_val is True:
                        return lbinds
                    if not self.fate:
                        continue
                    return logic_val

                if fact[1] == '<-':
                    if type(result) is not list:
                        if result is True:
                            return lbinds
                        continue
                    if result[0] is True:
                        self.op = '<-'
                        self.up_binds = lbinds
                        self.scope = result[1]
                        return self.scope_bind()
                    continue

                if fact[1] == '<-f':
                    if type(result) is not list:
                        if result is not False:
                            continue
                    if result[0] is not False:
                        continue
                    if not self.fate:
                        continue
                    return False
        self.fate = True
        return 'unknown'

class Scope:
    def __init__(self, base, queries, binds={}):
        self.first = binds
        self.queries = queries
        self.results = []
        self.searches = [Search(base, self.bind(queries[0]))]

    def resl_var(self, var):
        if var in self.first:
            var = self.first[var]
            if not val_is_var(var):
                return self.bind(var)
        for result in self.results:
            if not type(result) is dict:
                continue
            if var in result:
                var = binds[var]
                if not val_is_var(var):
                    return self.bind(var)
        return var

    def resl_list(self, query):
        new = []
        for val in query:
            new.append(self.bind(val))
        return new

    def bind(self, query):
        if val_is_const(query):
            return query
        if val_is_var(query):
            return self.resl_var(query)
        return self.resl_list(query)

    def latest_query(self):
        return self.bind(self.queries[len(self.searches)])

    def fated(self):
        for search in self.searches:
            if search.fate is False:
                return False
        return True

    def reverse_fate(self):
        while self.searches[-1].fate:
            self.searches.pop()
            self.results.pop()

    def final_result(self):
        final_result = True
        for result in self.results:
            if type(self.results) is dict:
                final_result = and1(final_result, True)
            else:
                final_result = and1(final_result, result)
        return final_result

    def run(self, base):
        if len(self.results) == len(self.queries):
            self.results.pop()

        while len(self.results) < len(self.queries):
            result = self.searches[-1].get(base)
            if type(result) is dict or self.fated():
                if len(self.searches) < len(self.queries):
                    self.searches.append(Search(base, self.latest_query()))
                self.results.append(result)
            else:
                self.reverse_fate()
        return self.final_result()
                
def unique_binds(val, binds):
    if val_is_var(val):
        if not val in binds:
            binds.add(val)
    elif type(val) is list:
        for sub_val in val:
            unique_binds(sub_val, binds)

def max_binds(val):
    binds = set([])
    unique_binds(val, binds)
    return len(binds)

def base_add(base, fact):
    fact_left = fact[0]
    left_max = max_binds(fact_left)
    for i in range(len(base)):
        lbinds = {}
        rbinds = {}
        if unify(fact_left, base[i][0], lbinds, rbinds):
            if len(lbinds) < len(rbinds):
                base.insert(i, fact)
                return
            if len(lbinds) == len(rbinds) and fact[1] == '<-':
                base.insert(i, fact)
                return
        else:
            right_max = max_binds(base[i][0])
            if left_max <= right_max:
                base.insert(i, fact)
                return
    base.append(fact)
            
base = []
    
base_add(base, [['human', 'Y'], '<-', [['woman', 'Y']]])
base_add(base, [['cat', 'socrates'], '=', False])
base_add(base, [['human', 'X'], '<-', [['man', 'X']]])
base_add(base, [['man', 'socrates'], '=', True])
base_add(base, [['likes', 'socrates', 'X'], '=', False])
base_add(base, [['woman', 'ophelia'], '=', True])
base_add(base, [['mortal', 'Z'], '<-', [['human', 'Z']]])
base_add(base, [['query', 'X'], '=', ['X']])
base_add(base, [['and', 'X', 'Y'],  '=', ['X', 'Y']])
# base_add(base, ['a', '=!', False])
base_add(base, [['not', 'X'], '=!', ['X']])
# lbinds = {}
# rbinds = {}

search = Search(base, ['X', 'socrates'])
result = search.get(base)
while type(result) is dict:
    print(result)
    result = search.get(base)

search = Search(base, ['not', ['query', ['not', ['cat', 'socrates']]]])
print(search.get(base))

# search = Search(base, ['query', ['cat', 'socrates']])
# print(search.get(base))
